T:Type, eq:EqDecider(T), L:(T List), i:int_seg(0; ||L||).
no_repeats(T; L)  (mu((i@0.eqof(eq)(L[i],L[i@0]))) = i  ) 

latex

Definitions	||as||, mu(f), no_repeats(T; l), type List, EqDecider(T), Type, , x.A(x), f(a), eqof(d), True, P  Q, b, x:A  B(x), P  Q, l[i], x:AB(x), void, #$n, a < b, x:A. B(x), t  T, int_seg(i; j), {x:A| B(x)} , lelt(i; j; k), A  B, P  Q, A, False, P  Q, s = t, , l_member!(x; l; T), (x  l), x:A. B(x), A c B, T
Lemmas	select member, no repeats member, length wf1, select wf, deq property, eqof eq btrue, int seg wf, eqof wf, assert wf, le wf, mu-bound-unique, deq wf, no repeats wf